Code (Week 3)

proctype A() {
    printf("Hello world, I am process %d!\n",_pid);
}

init {
    run A();
    run A();
}

#define TIMES 10
byte    n = 0;

proctype P() {
  byte i =0;
  byte temp;
  do 
  :: i < TIMES ->
    temp = n;
    n = temp + 1;
    i = i + 1;
  :: else -> break;
  od
}

init {
  atomic {
    run P();
    run P()
  }
  (_nr_pr == 1);
  printf("The value is %d\n", n);
  assert(n != 1)
}

inline critical_section() {
     printf("MSC: %d in CS\n", _pid);
}

inline non_critical_section() {
  printf("MSC: %d in non-CS\n", _pid);
  do               /* non-deterministically choose how
                      long to stay, even forever */
    :: true ->
         skip
    :: true ->
         break
  od
}

#include "critical2.h"

byte turn = 1;


active proctype p() {
  do
    :: non_critical_section();
wap:   turn == 1;               /* await */
csp:   critical_section(); 
       turn = 2
  od
}

active proctype q() {
  do
    :: non_critical_section();
waq:   turn == 2;               /* await */
csq:   critical_section();
       turn = 1
  od
}



ltl mutex { always (!(p@csp && q@csq)) }
ltl sfp {always (  p@wap implies eventually p@csp ) }
ltl sfq {always (  q@waq implies eventually q@csq ) }
/*
We can use an auxiliary variable with a monitor process like so:
active proctype monitor() {
    do
    :: assert(inCS != 2);
    od
}
*/

/*
A more idiomatic way is to use never claims
never {
    do :: inCS >= 2 -> break
       :: else 
    od
}

We can avoid auxiliary variables using label assertions:
never {
    do :: p@csp && q@csq -> break
       :: else 
    od
}

We can also just state LTL directly as above.
*/

#include "critical2.h"

bool wantp = false, wantq = false;

active proctype p() {
  do
    :: non_critical_section();
wap:   wantp = true; 
       wantq == false;  /* await */
csp:   critical_section();
       wantp = false
  od
}

active proctype q() {
  do
    :: non_critical_section();
       /* Originally this came before the await,
           but it lead to mutex violation */
waq:   wantq = true;
       wantp == false; /* await */
csq:   critical_section();
       wantq = false
  od
}
ltl mutex { always (!(p@csp && q@csq)) }

#include "critical2.h"
byte wantp = 0;
byte wantq = 0;
byte turn = 1;
active proctype p() {
  do
    :: non_critical_section();
wap:   wantp = true; turn = 1;
       (wantq == false) || (turn == 0);
csp:   critical_section(); 
       wantp = false;
  od
}

active proctype q() {
  do
    :: non_critical_section();
waq:   wantq = true; turn = 0;
       (wantp == false) || (turn == 1);
csq:   critical_section();
       wantq = false;
  od
}

ltl mutex { always (!(p@csp && q@csq)) }
ltl sf { always (p@wap implies eventually p@csp)}

/* needs fairness for sf */

#include "critical2.h"
mtype = {LOCK, UNLOCK};

proctype lock( chan l ) {
    do :: l ? LOCK; l ? UNLOCK; od 
}
proctype p(chan l) {
  do
    :: non_critical_section();
wap:   l ! LOCK;
csp:   critical_section(); 
       l ! UNLOCK;
  od
}

proctype q(chan l) {
  do
    :: non_critical_section();
waq:   l ! LOCK;
csq:   critical_section();
       l ! UNLOCK;
  od
}

init {
    chan l = [0] of { mtype };
    run p(l);
    run q(l);
}

ltl mutex { [](!(p@csp && q@csq)) }

#include "critical2.h"
proctype p(chan l) {
  do
    :: non_critical_section();
wap:   l ? 1;
csp:   critical_section(); 
       l ! 1;
  od
}

proctype q(chan l) {
  do
    :: non_critical_section();
waq:   l ? 1;
csq:   critical_section();
       l ! 1;
  od
}

init {
    chan l = [1] of { bit };
    l!1;
    run p(l);
    run q(l);
}

ltl mutex { [](!(p@csp && q@csq)) }